feat(bivariate): approximant-basis and hybrid GS interpolation - #291

CompPoly/Bivariate/GuruswamiSudan/Interpolation/LeeOSullivan/Basic.lean (3)

• def distinctXCoordinatesBool {F : Type*} [BEq F] (points : Array (F × F)) : Bool
• def distinctXCoordinatesListBool {F : Type*} [BEq F] : List (F × F) → Bool
• def interpolationYCap (params : GSInterpParams) : Nat

CompPoly/Bivariate/Deriv.lean (3)

• theorem shiftC_add [CommSemiring R] [BEq R] [LawfulBEq R] [Nontrivial R] [DecidableEq R]
• theorem shiftC_mul [CommSemiring R] [BEq R] [LawfulBEq R] [Nontrivial R]
• theorem toPoly_injective [Semiring R] [BEq R] [LawfulBEq R] [Nontrivial R]

CompPoly/Bivariate/GuruswamiSudan/Implementations.lean (21)

• def approximantPMBasisComposeLeafCutoff : Nat
• def approximantPMBasisLeafCutoff : Nat
• def fastKoalaBearAlekhnovichNttFastRootContext : GSRootContext KoalaBear.Fast.Field
• def fastKoalaBearAlekhnovichRootContext : GSRootContext KoalaBear.Fast.Field
• def fastKoalaBearApproximantBasisDirectInterpContext :
• def fastKoalaBearApproximantBasisInterpContext :
• def fastKoalaBearApproximantBasisSubproductInterpContext :
• def fastKoalaBearApproximantPMBasisContext :
• def fastKoalaBearApproximantSolutionContext :
• def fastKoalaBearHybridInterpContext : GSInterpContext KoalaBear.Fast.Field
• def fastKoalaBearNttFastLowMulContext :
• def hybridReductionStepBudget (params : GSInterpParams) : Nat
• def koalaBearAlekhnovichNttFastRootContext : GSRootContext KoalaBear.Field
• def koalaBearAlekhnovichRootContext : GSRootContext KoalaBear.Field
• def koalaBearApproximantBasisDirectInterpContext : GSInterpContext KoalaBear.Field
• def koalaBearApproximantBasisInterpContext : GSInterpContext KoalaBear.Field
• def koalaBearApproximantBasisSubproductInterpContext : GSInterpContext KoalaBear.Field
• def koalaBearApproximantPMBasisContext :
• def koalaBearApproximantSolutionContext :
• def koalaBearHybridInterpContext : GSInterpContext KoalaBear.Field
• def koalaBearNttFastLowMulContext :

CompPoly/Bivariate/GuruswamiSudan/Interpolation/ApproximantBasis/Algorithm.lean (3)

• def approximantBasisInterpolate
• def approximantBasisPositiveInterpolate
• def normalizeApproximantCandidate? (params : GSInterpParams) (Q : CBivariate F) :

CompPoly/Bivariate/GuruswamiSudan/Interpolation/ApproximantBasis/Basic.lean (8)

• def buildGSModularDataWithRG
• def buildGSModularData
• def gsModuli (mulCtx : CPolynomial.MulContext F) (G : CPolynomial F) (s : Nat) :
• def gsRelationColumn (mulCtx : CPolynomial.MulContext F)
• def gsRelationEntry (modCtx : CPolynomial.ModContext F)
• def gsRelationMatrixWithModuli (mulCtx : CPolynomial.MulContext F)
• def gsRelationMatrixWithRG (mulCtx : CPolynomial.MulContext F)
• def modularEquation (data : GSModularData F) : ModularEquation F

CompPoly/Bivariate/GuruswamiSudan/Interpolation/ApproximantBasis/Correctness.lean (16)

• def approximantBasisInterpContext
• private theorem coeff_eq_zero_of_interpolationWidth_le
• private theorem coeff_toCoeffRow_ofCoeffRow (row : PolynomialRow F)
• private theorem interpolationCoefficientVector_toCoeffRow (params : GSInterpParams)
• private theorem interpolationMonomials_yDegree_lt (params : GSInterpParams)
• private theorem normalizeInterpolationPolynomial?_eq_none_of_rowIsZero
• private theorem normalizeVector?_eq_none_of_all_zero {v : Array F}
• private theorem ofCoeffRow_eq_zero_of_rowIsZero {row : PolynomialRow F}
• private theorem ofCoeffRow_toCoeffRow_eq
• private theorem rowGet_toCoeffRow_ofCoeffRow (row : PolynomialRow F)
• private theorem rowShiftedDegree?_congr_shift {row : PolynomialRow F}
• private theorem rowShiftedDegree?_toCoeffRow_le {row : PolynomialRow F}
• private theorem weightedDegreeShift_getD {w width j : Nat} (hj : j < width) :
• theorem approximantBasisInterpolate_complete
• theorem approximantBasisInterpolate_sound
• theorem gsModularEquation_row_iff_multiplicity

CompPoly/Bivariate/GuruswamiSudan/Interpolation/ApproximantBasis/ModularData.lean (33)

• private def relationColumnStep (mulCtx : CPolynomial.MulContext F)
• private theorem dvd_iff_dvd_of_dvd_sub {M a b : Polynomial F} (h : M ∣ a - b) :
• private theorem foldl_add_eq_sum {M : Type*} [AddCommMonoid M] (f : Nat → M) :
• private theorem foldl_mprod_fst {α β : Type u} {γ : Type*}
• private theorem gsModuli_loop (mulCtx : CPolynomial.MulContext F) (G : CPolynomial F) :
• private theorem gsRelationColumn_eq_foldl (mulCtx : CPolynomial.MulContext F)
• private theorem relationColumn_foldl_size_untouched (mulCtx : CPolynomial.MulContext F)
• private theorem relationColumn_foldl_spec (mulCtx : CPolynomial.MulContext F)
• private theorem rowGet_rowMulMatrixWith_eq_sum (mulCtx : CPolynomial.MulContext F)
• private theorem rowMulMatrix_foldl_eq_sum_size (mulCtx : CPolynomial.MulContext F)
• private theorem rowSatisfiesModularBool_iff_forall (mulCtx : CPolynomial.MulContext F)
• private theorem toPoly_finset_sum (f : Nat → CPolynomial F) (n : Nat) :
• private theorem toPoly_ofCoeffRow_eq_sum (row : PolynomialRow F) :
• theorem dvd_modByMonicWith_sub (modCtx : CPolynomial.ModContext F)
• theorem gsModuli_eq (mulCtx : CPolynomial.MulContext F) (G : CPolynomial F) (s : Nat) :
• theorem gsModuli_getD (mulCtx : CPolynomial.MulContext F) (G : CPolynomial F)
• theorem gsModuli_getD_one (mulCtx : CPolynomial.MulContext F) (G : CPolynomial F)
• theorem gsModuli_size (mulCtx : CPolynomial.MulContext F) (G : CPolynomial F) (s : Nat) :
• theorem gsRelationColumn_getD_congr (mulCtx : CPolynomial.MulContext F)
• theorem gsRelationColumn_getD_of_lt (mulCtx : CPolynomial.MulContext F)
• theorem gsRelationColumn_size (mulCtx : CPolynomial.MulContext F)
• theorem gsRelationMatrixWithModuli_entry (mulCtx : CPolynomial.MulContext F)
• theorem gsRelationMatrixWithModuli_matrixWidth (mulCtx : CPolynomial.MulContext F)
• theorem gsRelationMatrixWithModuli_size (mulCtx : CPolynomial.MulContext F)
• theorem hasseDeriv_toPoly_ofCoeffRow_eval (row : PolynomialRow F)
• theorem modByMonicWith_eq_zero_iff_dvd (modCtx : CPolynomial.ModContext F)
• theorem modByMonicWith_toPoly (modCtx : CPolynomial.ModContext F)
• theorem ofFn_matrixWidth (rows width : Nat) (entry : Nat → Nat → CPolynomial F)
• theorem ofFn_rowGet (rows width : Nat) (entry : Nat → Nat → CPolynomial F)
• theorem ofFn_size (rows width : Nat) (entry : Nat → Nat → CPolynomial F) :
• theorem rowMulMatrixWith_congr_of_agree (mulCtx : CPolynomial.MulContext F)
• theorem rowSatisfiesModularBool_congr_of_agree (mulCtx : CPolynomial.MulContext F)
• theorem rowSatisfiesModularBool_gsRelationMatrix_iff

CompPoly/Bivariate/GuruswamiSudan/Interpolation/ApproximantBasis/Multiplicity.lean (9)

• private theorem vanishingPolynomialArray_toPoly_list
• theorem X_sub_C_pow_dvd_hasseDeriv_eval_iff_hasMultiplicity
• theorem X_sub_C_pow_dvd_hasseDeriv_eval_of_dvd_sub
• theorem X_sub_C_pow_dvd_iff_hasseDeriv_eval_eq_zero
• theorem linearFactor_toPoly_eq (x : F) :
• theorem prod_X_sub_C_pow_dvd_of_nodup
• theorem vanishingPolynomialArray_toPoly (xs : Array F) :
• theorem vanishingPolynomialArray_toPoly_monic (xs : Array F) :
• theorem vanishing_pow_dvd_hasseDeriv_eval_iff_satisfiesMultiplicityConstraints

CompPoly/Bivariate/GuruswamiSudan/Interpolation/Basic.lean (5)

• def distinctXCoordinatesBool {F : Type*} [BEq F] (points : Array (F × F)) : Bool
• def distinctXCoordinatesListBool {F : Type*} [BEq F] : List (F × F) → Bool
• def interpolationShifts (params : GSInterpParams) : Array Nat
• def interpolationWidth (params : GSInterpParams) : Nat
• def interpolationYCap (params : GSInterpParams) : Nat

CompPoly/Bivariate/GuruswamiSudan/Interpolation/Hybrid/Algorithm.lean (2)

• def hybridInterpolate
• def hybridPositiveInterpolate

CompPoly/Bivariate/GuruswamiSudan/Interpolation/Hybrid/Correctness.lean (4)

• def hybridInterpContext
• private theorem hybrid_probe_eq_reduceFast
• theorem hybridInterpolate_eq_lee_or_approximant
• theorem hybridPositiveInterpolate_eq_lee_or_approximant

CompPoly/Bivariate/GuruswamiSudan/Interpolation/WitnessDivisibility.lean (4)

• def divByLinearYWith {R : Type*} [Semiring R] [BEq R] [LawfulBEq R] [Nontrivial R]
• def interpolationWitnessIsValidViaDivisibilityBool {F : Type*}
• def satisfiesMultiplicityConstraintsViaDivisibilityBool {F : Type*}
• theorem divByLinearYWith_eq_divByLinearY {R : Type*}

CompPoly/Bivariate/GuruswamiSudan/Interpolation/WitnessDivisibilityCorrectness.lean (27)

• private theorem witness_coeff_linearYDivisor (u : CPolynomial F) (j : Nat) :
• private theorem witness_coeff_low_vanish
• private theorem witness_coeff_sub (p q : CPolynomial F) (i : Nat) :
• private theorem witness_cpoly_eq_of_toPoly_eq {R : Type*}
• private theorem witness_divByLinearY_decomposition (Q : CBivariate F)
• private theorem witness_foldl_linearFactor_monic (l : List F) (acc : CPolynomial F)
• private theorem witness_hasMultiplicityAtLeast_C_of_dvd
• private theorem witness_hasMultiplicityAtLeast_add
• private theorem witness_hasMultiplicityAtLeast_sub
• private theorem witness_hasMultiplicityAtLeast_zero (P : CBivariate F) (x y : F) :
• private theorem witness_hasMultiplicity_quot
• private theorem witness_linearFactor_toPoly (x : F) :
• private theorem witness_modByMonic_eq_zero_iff {c g : CPolynomial F}
• private theorem witness_monic_pow {g : CPolynomial F} (hg : g.monic) (k : Nat) :
• private theorem witness_ofYConstant_pow (G : CPolynomial F) (k : Nat) :
• private theorem witness_outerCoeff_linearYDivisor_mul (u : CPolynomial F)
• private theorem witness_outerCoeff_shiftC_C (x y : F) (c : CPolynomial F)
• private theorem witness_shiftC_linearYDivisor (x y : F) (R : CPolynomial F) :
• private theorem witness_shiftX_linearYDivisor (x : F) (u : CPolynomial F) :
• private theorem witness_shiftY_linearYDivisor (y : F) (R : CPolynomial F) :
• private theorem witness_taylor_neg (x : F) (u : CPolynomial F) :
• private theorem witness_taylor_one (x : F) :
• private theorem witness_taylor_sub_C (x y : F) (R : CPolynomial F) :
• private theorem witness_vanishing_monic (xs : Array F) :
• private theorem witness_viaDivisibility_iff
• theorem interpolationWitnessIsValidViaDivisibilityBool_eq
• theorem satisfiesMultiplicityConstraintsViaDivisibilityBool_eq

CompPoly/LinearAlgebra/PolynomialMatrix/Approximant/Basic.lean (7)

• def lowerOrders [Zero F] (problem : XAdicProblem F) (d : Nat) : Array Nat
• def maxOrder [Zero F] (problem : XAdicProblem F) : Nat
• def residualMatrix [Semiring F] [BEq F] [LawfulBEq F]
• def residualMatrixWithProduct [Semiring F] [BEq F] [LawfulBEq F]
• def residualOrders [Zero F] (problem : XAdicProblem F) (d : Nat) : Array Nat
• def totalOrder [Zero F] (problem : XAdicProblem F) : Nat
• def updateShiftByRows [Zero F] [BEq F]

CompPoly/LinearAlgebra/PolynomialMatrix/Approximant/Correctness.lean (2)

• theorem modularSolutionBasis_complete_minimal
• theorem modularSolutionBasis_sound

CompPoly/LinearAlgebra/PolynomialMatrix/Approximant/ModularEquation.lean (1)

• def modularSolutionBasisContextViaPMBasis

CompPoly/LinearAlgebra/PolynomialMatrix/Approximant/ModularEquation/Basic.lean (53)

• def ModularEquation.modularWidth (equation : ModularEquation F) : Nat
• def ModularEquation.solutionWidth (equation : ModularEquation F) : Nat
• def PivotDegreeProfile.coversAll (profile : PivotDegreeProfile) : Bool
• def PivotDegreeProfile.discoveredAny (profile : PivotDegreeProfile) : Bool
• def PivotDegreeProfile.insert (profile : PivotDegreeProfile)

…and 598 more not listed.

• theorem eval_hasseDeriv_eval_hasseDeriv_toPoly {F : Type*} in CompPoly/Bivariate/GuruswamiSudan/PolynomialCorrectness.lean moved from L931 to L931

• CompPoly.lean: The diff adds approximately 30 new public imports to the file's import block. The new imports are concentrated in two main areas: the CompPoly.Bivariate.GuruswamiSudan interpolation submodule (adding Interpolation itself, ApproximantBasis and its submodules Algorithm, Basic, Correctness, ModularData, Multiplicity, Hybrid and its submodules Algorithm, Correctness, plus WitnessDivisibility and WitnessDivisibilityCorrectness) and the CompPoly.LinearAlgebra.PolynomialMatrix approximant submodule (adding Approximant and its submodules Basic, Correctness, ModularEquation, ModularEquation.Basic, ModularEquation.Completeness, PMBasis and its submodules Correctness, KernelLeaf, KernelLeafCompleteness, KernelLeafScalar, KernelLeafSoundness, KernelLeafSpan, Recursion, XAdicSoundness, PartialLinearization, plus Operations, RowSelection, and StrassenCorrectness). The diff also adds MuldersStorjohannCorrectness.WeakPopovMinimal and removes nothing. These are all import additions — no theorems, definitions, or proof bodies are modified, and no sorry or admit statements are introduced by this change.
• CompPoly/Bivariate/Deriv.lean: The diff adds three theorems to CompPoly/Bivariate/Deriv.lean:

• toPoly_injective: proves that toPoly : CBivariate R → Polynomial (Polynomial R) is injective (via toPoly_ofPoly).
• shiftC_add and shiftC_mul: prove that the generic Taylor shift shiftC a b is additive and multiplicative, respectively; both proofs use toPoly_injective to reduce to the additive (Polynomial.add_comp, Polynomial.map_add) and multiplicative (Polynomial.mul_comp, Polynomial.map_mul) properties of the underlying polynomial shift.

No sorry or admit appear in the diff.

• CompPoly/Bivariate/GuruswamiSudan/Implementations.lean: Adds 16 new definitions and 4 new public imports. The public imports expose correctness theorems for hybrid interpolation and Alekhnovich root-finding. New MulLowContext definitions (koalaBearNttFastLowMulContext, fastKoalaBearNttFastLowMulContext) provide low-degree polynomial multiplication backends. Two cutoff constants (approximantPMBasisLeafCutoff, approximantPMBasisComposeLeafCutoff) configure approximant-basis PM recursion. Two PM-basis contexts (koalaBearApproximantPMBasisContext, fastKoalaBearApproximantPMBasisContext) and two modular-solution contexts (koalaBearApproximantSolutionContext, fastKoalaBearApproximantSolutionContext) support the approximant-basis interpolation. Six GSInterpContext definitions (three per field variant: koalaBearApproximantBasisDirectInterpContext, koalaBearApproximantBasisSubproductInterpContext, koalaBearApproximantBasisInterpContext, and their fast counterparts) bundle vanishing-polynomial and batch-evaluation strategies for the approximant-basis backend. A hybridReductionStepBudget function defines the ski-rental break-even point for hybrid interpolation. Two hybrid GSInterpContext definitions (koalaBearHybridInterpContext, fastKoalaBearHybridInterpContext) combine budgeted Lee-O'Sullivan reduction with approximant fallback. Four Alekhnovich GSRootContext definitions (canonical/NTTFast for both field variants) provide the Alekhnovich root-finding backend. No sorry or admit statements were introduced.
• CompPoly/Bivariate/GuruswamiSudan/Interpolation.lean: This new file aggregates and publicly re-exports correctness modules for multiple Guruswami–Sudan interpolation backends: Dense, LeeOSullivan, ApproximantBasis, Hybrid, and a generic Correctness. By using public import and an @[expose] public section, it provides a unified entry point that exposes all backend correctness proofs as part of the public API. No sorry or admit statements appear; the file is purely a re‑export surface.
• CompPoly/Bivariate/GuruswamiSudan/Interpolation/ApproximantBasis.lean: Added a new top-level module file ApproximantBasis.lean that publicly re-exports the Basic, Algorithm, and Correctness submodules of the Guruswami–Sudan interpolation approximant basis development. The file includes an @[expose] public section command to expose the section, thereby providing a single import point for the entire approximant basis theory.
• CompPoly/Bivariate/GuruswamiSudan/Interpolation/ApproximantBasis/Algorithm.lean: This new file adds three executable definitions for the approximant-basis interpolation step of the Guruswami–Sudan algorithm. normalizeApproximantCandidate? normalizes a row-derived candidate using the interpolation coefficient vector. approximantBasisPositiveInterpolate builds modular equations from vanishing polynomials and a batch evaluation context, solves them via a provided solver context, selects the least shifted-degree row, and normalizes the result. approximantBasisInterpolate dispatches to a low‑message‑degree branch when params.messageDegree ≤ 1 and otherwise delegates to the positive branch. No sorry or admit appear.
• CompPoly/Bivariate/GuruswamiSudan/Interpolation/ApproximantBasis/Basic.lean: New file Basic.lean introduces the data structures and construction functions for the approximant-basis interpolation backend of the Guruswami–Sudan algorithm. It defines gsModuli to compute column moduli G^(s-b) by iterated multiplication, gsRelationEntry and gsRelationColumn to build entries and columns of the binomial relation matrix, and gsRelationMatrixWithModuli/gsRelationMatrixWithRG to assemble the full matrix from precomputed moduli. The GSModularData structure holds G, R, moduli, matrix, and shift array, with buildGSModularDataWithRG constructing it from R and G, and buildGSModularData from evaluation points. modularEquation provides a view as a ModularEquation. No sorry or admit appear.
• CompPoly/Bivariate/GuruswamiSudan/Interpolation/ApproximantBasis/Correctness.lean: This new file CompPoly/Bivariate/GuruswamiSudan/Interpolation/ApproximantBasis/Correctness.lean proves the soundness (approximantBasisInterpolate_sound) and completeness (approximantBasisInterpolate_complete) of the executable approximantBasisInterpolate routine. It defines several supporting lemmas: rowGet_toCoeffRow_ofCoeffRow and coeff_toCoeffRow_ofCoeffRow relate the entries of a row and its width-truncated version; interpolationCoefficientVector_toCoeffRow shows the interpolation coefficient vector ignores the truncated coefficients; rowShiftedDegree?_toCoeffRow_le ensures the shifted row degree does not increase under truncation; normalizeVector?_eq_none_of_all_zero and normalizeInterpolationPolynomial?_eq_none_of_rowIsZero handle the case of zero rows; and gsModularEquation_row_iff_multiplicity equates the modular predicate to multiplicity constraints. The completeness theorem also uses coe f_eq_zero_of_interpolationWidth_le and ofCoeffRow_toCoeffRow_eq to argue that the witness polynomial’s row truncation is faithful. Finally, the file constructs the public approximantBasisInterpContext wrapping the two theorems into a GSInterpContext. No sorry or admit appear in the diff.
• CompPoly/Bivariate/GuruswamiSudan/Interpolation/ApproximantBasis/ModularData.lean: This file introduces new executable bridges for GS modular data, defining and proving semantic correctness of the modulus array gsModuli, the relation column gsRelationColumn, the relation matrix gsRelationMatrixWithModuli, and the row predicate rowSatisfiesModularBool. It adds the following new theorems to the namespace CompPoly.GuruswamiSudan.ApproximantBasis: gsModuli_eq, gsModuli_size, gsModuli_getD, gsModuli_getD_one, gsRelationColumn_size, gsRelationColumn_getD_of_lt, gsRelationColumn_getD_congr, gsRelationMatrixWithModuli_entry, gsRelationMatrixWithModuli_size, gsRelationMatrixWithModuli_matrixWidth, hasseDeriv_toPoly_ofCoeffRow_eval, rowMulMatrixWith_congr_of_agree, rowSatisfiesModularBool_congr_of_agree, and rowSatisfiesModularBool_gsRelationMatrix_iff. The main result rowSatisfiesModularBool_gsRelationMatrix_iff establishes that the executable modular row predicate over the GS relation matrix and modulus array is equivalent to divisibility of every sheared coefficient (hasseDeriv b (ofCoeffRow row).toPoly).eval R by G^(s-b). There are no sorry or admit remaining in this file.
• CompPoly/Bivariate/GuruswamiSudan/Interpolation/ApproximantBasis/Multiplicity.lean: This new file adds the core 'shear equivalence' theorem vanishing_pow_dvd_hasseDeriv_eval_iff_satisfiesMultiplicityConstraints and its supporting lemmas for the Guruswami–Sudan approximant-basis backend. The main theorem states that for a set of points with distinct x-coordinates and an interpolating polynomial R, the family of Hasse-derivative evaluations (hasseDeriv b Q.toPoly).eval R.toPoly being divisible by G^(s-b) (where G is the vanishing polynomial of the x-coordinates) is equivalent to the packed GS multiplicity constraints CBivariate.SatisfiesMultiplicityConstraints Q points s. Supporting lemmas include: X_sub_C_pow_dvd_iff_hasseDeriv_eval_eq_zero (characterising (X-x)^k divisibility via Hasse-derivative vanishing), X_sub_C_pow_dvd_hasseDeriv_eval_of_dvd_sub (transferring the divisibility family between evaluation points agreeing modulo X-x), X_sub_C_pow_dvd_hasseDeriv_eval_iff_hasMultiplicity (the single-node equivalence), linearFactor_toPoly_eq (identifying the toPoly of a linear factor with X - C x), vanishingPolynomialArray_toPoly and vanishingPolynomialArray_toPoly_monic (describing the array vanishing polynomial under toPoly), and prod_X_sub_C_pow_dvd_of_nodup (gluing per-factor divisibility into a product-of-distinct-factors divisibility). No sorry or admit are present.
• CompPoly/Bivariate/GuruswamiSudan/Interpolation/Basic.lean: The diff adds a public import of CompPoly.Bivariate.CoeffRows and introduces five new definitions: interpolationYCap (the Y cap computed as weightedDegreeBound / yWeight), interpolationWidth (the number of coefficient columns, equal to the Y cap + 1), interpolationShifts (an array of shifts produced by weightedDegreeShift), and two executable duplicate-x coordinate detectors, distinctXCoordinatesListBool (list-based) and distinctXCoordinatesBool (array-based, delegating to the list version). These additions provide the Y‑capped width and shift structure needed by positive‑Y‑weight interpolation backends and an executable check for distinct x‑coordinates in point sets. No sorry or admit are present.
• CompPoly/Bivariate/GuruswamiSudan/Interpolation/Hybrid.lean: Summary unavailable — AI generation failed.
• CompPoly/Bivariate/GuruswamiSudan/Interpolation/Hybrid/Algorithm.lean: This new file implements the hybrid Guruswami–Sudan interpolation backend, adding two definitions. hybridPositiveInterpolate runs the Lee‑O’Sullivan reduction with a caller‑provided step budget (budget : GSInterpParams → Nat); if the budget is exhausted before the basis becomes conflict‑free, it falls back to the approximant‑basis solver. hybridInterpolate dispatches to a simpler low‑message‑degree interpolation when params.messageDegree ≤ 1 and otherwise delegates to hybridPositiveInterpolate. The file also includes module‑level documentation explaining the ski‑rental budget policy and providing references.
• CompPoly/Bivariate/GuruswamiSudan/Interpolation/Hybrid/Correctness.lean: This new file Correctness.lean proves the correctness of the hybrid Guruswami–Sudan interpolation backend (hybridInterpContext). It introduces a private lemma hybrid_probe_eq_reduceFast that equates the budgeted Mulders–Storjohann reduction to the full fast reduction when no shifted leading conflict is cached. Using this, it establishes two main theorems: hybridPositiveInterpolate_eq_lee_or_approximant and hybridInterpolate_eq_lee_or_approximant, each stating that the corresponding hybrid interpolation function equals either the Lee–O'Sullivan result (with the fast reducer context) or the approximant-basis result. Finally, it defines the hybridInterpContext structure, which provides the interpolate method and proves its sound and complete properties by case-analyzing on those two theorems and delegating to the known correctness proofs of the two backends. No sorry or admit appears in the diff.
• CompPoly/Bivariate/GuruswamiSudan/Interpolation/LeeOSullivan/Basic.lean: Removed the definition interpolationYCap (which provided a finite Y cap for positive-Y-weight interpolation backends) and the auxiliary functions distinctXCoordinatesListBool and distinctXCoordinatesBool (executable duplicate-x detectors for packed points).
• CompPoly/Bivariate/GuruswamiSudan/Interpolation/WitnessDivisibility.lean: Added the new file WitnessDivisibility.lean providing a divisibility-based efficiency improvement for checking Guruswami-Sudan multiplicity constraints. It defines divByLinearYWith (synthetic division using an explicit multiplication context) and proves divByLinearYWith_eq_divByLinearY equating it to the existing divByLinearY. It then defines satisfiesMultiplicityConstraintsViaDivisibilityBool, which tests multiplicity by checking divisibility of the base-(Y - R) digits by powers of G, and interpolationWitnessIsValidViaDivisibilityBool, which combines this with nonzero and weighted-degree checks as a fast alternative to the per-point Hasse derivative loop. No sorry or admit are present.
• CompPoly/Bivariate/GuruswamiSudan/Interpolation/WitnessDivisibilityCorrectness.lean: This new file (509 lines) proves the equivalence of two multiplicity-checking algorithms for the Guruswami–Sudan interpolation step in a Lean 4 formalization. It defines witness_viaDivisibility_iff, satisfiesMultiplicityConstraintsViaDivisibilityBool_eq, and interpolationWitnessIsValidViaDivisibilityBool_eq, establishing that the divisibility-based witness check (satisfiesMultiplicityConstraintsViaDivisibilityBool) agrees with the pointwise Hasse derivative check (CBivariate.satisfiesMultiplicityConstraintsBool) on point sets with distinct x-coordinates, and consequently that interpolationWitnessIsValidViaDivisibilityBool agrees with interpolationWitnessIsValidBool. The proof uses several auxiliary lemmas (e.g., witness_modByMonic_eq_zero_iff, witness_hasMultiplicity_quot, witness_hasMultiplicityAtLeast_add, witness_coeff_low_vanish) to handle the Euclidean division by (Y - R), coefficient-level vanishing arguments, and the induction on multiplicity levels. No sorry or admit appear in the diff.
• CompPoly/Bivariate/GuruswamiSudan/PolynomialCorrectness.lean: The visibility of eval_hasseDeriv_eval_hasseDeriv_toPoly was changed from private to public, exporting a theorem that equates the univariate X-Hasse derivative of the evaluated Y-Hasse derivative to the executable bivariate Hasse derivative. This makes a correctness lemma about double Hasse derivative evaluation accessible outside the file, likely required for downstream reasoning in the Guruswami–Sudan algorithm.
• CompPoly/LinearAlgebra/PolynomialMatrix.lean: This diff adds two new public imports to the PolynomialMatrix module: CompPoly.LinearAlgebra.PolynomialMatrix.Operations and CompPoly.LinearAlgebra.PolynomialMatrix.Approximant. These imports expose the definitions and theorems from the Operations and Approximant modules, which are now part of the module's public API.
• CompPoly/LinearAlgebra/PolynomialMatrix/Approximant.lean: This new file Approximant.lean acts as a top-level re‑exporter for the Approximant polynomial‑matrix subdirectory. It publicly re‑imports five submodules — Basic, PMBasis, PartialLinearization, ModularEquation, and Correctness — and declares a @[expose] public section, making the entire infrastructure available under the CompPoly.LinearAlgebra.PolynomialMatrix.Approximant namespace. No theorems, definitions, or proofs are added; the file purely organizes and exposes the existing submodules.
• CompPoly/LinearAlgebra/PolynomialMatrix/Approximant/Basic.lean: This new file introduces the XAdicProblem structure for row approximant problems and several helper functions in the PolynomialMatrix.Approximant namespace: maxOrder and totalOrder compute the maximum and sum of the problem's orders; lowerOrders and residualOrders truncate or decrement orders by a given d. The function updateShiftByRows adjusts a shift array based on row degrees of a basis matrix, and both residualMatrixWithProduct (with an explicit product kernel) and residualMatrix (using the direct low-product kernel) compute the residual (P * A) div X^d with columnwise truncation to the given orders. The file also uses @[expose] public section to control visibility.
• CompPoly/LinearAlgebra/PolynomialMatrix/Approximant/Correctness.lean: This file introduces a new public-facing theorem surface for the X-adic approximant correctness proofs. It re-exports the ModularEquation namespace, then defines two theorems that delegate directly to existing methods on ModularSolutionBasisContext: modularSolutionBasis_sound (proves any row from the solution basis satisfies the modular equation) and modularSolutionBasis_complete_minimal (proves the basis is complete and minimal relative to a caller-supplied degree bound, returning both a width bound for all basis rows and an existential witness for a matching row). These theorems provide a stable, executable entry point for the invariant that the modular solution basis yields exactly the rows satisfying the modular equation under the given bounds.
• CompPoly/LinearAlgebra/PolynomialMatrix/Approximant/ModularEquation.lean: This new file adds the definition modularSolutionBasisContextViaPMBasis which constructs a ModularSolutionBasisContext from a given multiplication context, modular context, and X-adic PM-basis context. The definition fills in the solutionBasis field with filteredSolutionBasisViaPMBasis, and provides proofs for the sound and complete_minimal fields. The sound proof delegates directly to filteredSolutionBasisViaPMBasis_sound, while the complete_minimal proof — the bulk of the file — is a lengthy case analysis handling two main branches based on degreeGatePassed: when the degree gate is passed it uses the adaptive solution basis; when the gate fails or no bound is supplied it constructs a certified union, with further subcases depending on whether a bound is provided, whether the solution fits the gated window, and whether an adaptive row already dominates. The module also includes a docstring and the copyright header.
• CompPoly/LinearAlgebra/PolynomialMatrix/Approximant/ModularEquation/Basic.lean: This new 769-line file introduces the ModularEquation solver framework. It defines the ModularEquation structure, the PivotDegreeProfile structure, and the core solver functions filteredSolutionBasisViaPMBasis (the main production entry point for computing a basis of rows satisfying the diagonal modular equation) and its supporting adaptive window-escalation loop (adaptiveSolutionBasis, adaptiveSolutionRound, adaptiveSolutionLoop). The file also provides a certified fallback solver (windowedSolutionBasisViaPMBasis), a residual repair pass (repairSolutionRowsViaPMBasis), a debug unchunked solver (debugUnchunkedFilteredSolutionBasisViaPMBasis), the ModularSolutionBasisContext structure bundling the solver with soundness and completeness/minimality theorems, and the accompanying soundness proofs (filteredSolutionBasisViaPMBasis_sound, etc.). The complementary degreeGatePassed and gatedWindowBound utilities allow a caller-supplied degree bound to short-circuit the certification step. No sorry or admit are present in the diff.
• CompPoly/LinearAlgebra/PolynomialMatrix/Approximant/ModularEquation/Completeness.lean: 新增文件 CompPoly/LinearAlgebra/PolynomialMatrix/Approximant/ModularEquation/Completeness.lean 证明了过滤后 PM-基模求解器的完备性/极小性。关键定理 me_verification_dominates 指出：对于给定的单次对角模方程，任何非零的等宽模解行，如果其移位次数在验证窗口 bound 内，则被过滤验证基中的某一行所支配（其移位次数不超过原行的移位次数）。辅助定理 me_prodRow_facts 构造了回退行 e_p * prod(moduli) 并证明其满足模方程、非零且移位次数有界。此外，me_adaptiveBasis_width 确保自适应解基的所有行都具有相同的线性宽度。文件中还包含大量私有引理，覆盖了 getD、rowGet、rowIsZero、rowShiftedDegree? 等辅助性质，以及 me_moduliProduct 和 me_moduliProduct_dvd 等与模数乘积相关的定义。
• CompPoly/LinearAlgebra/PolynomialMatrix/Approximant/PMBasis.lean: This new file adds three public PMBasisContext definitions — kernelLeafPMBasisContextWithLowAndCompose, kernelLeafPMBasisContextWithLow, and kernelLeafPMBasisContext — that bundle a recursive PM‑basis driver (with scalar dense‑kernel leaves) together with correctness proofs (sound, complete_minimal) imported from CompPoly.LinearAlgebra.PolynomialMatrix.Approximant.PMBasis.Correctness. The first definition is fully parameterized by independent leaf and composition cutoffs; the second sets both cutoffs equal; the third supplies the low‑product context via PolynomialMatrix.MulLowContext.fromMulContext. These contexts make the divide‑and‑conquer approximant‑basis algorithm available at the top‑level API for use in subsequent polynomial‑matrix computations. No sorry or admit appear in the file.
• CompPoly/LinearAlgebra/PolynomialMatrix/Approximant/PMBasis/Correctness.lean: This file proves soundness, completeness, and shifted minimality for the kernel-leaf recursive PM-basis construction. Several new theorems establish the core results: pmBasisWithFuelCore_kernelLeaf_rows shows every row of the fuel-bounded core approximates the problem and has the principal width; pmBasis_kernelLeaf_approximates derives the same for the root-normalized final basis; pmBasisWithFuelCore_kernelLeaf_rowSpan_complete proves that every nonzero X-adic solution row lies in the row-span of the core; and pmBasis_kernelLeaf_complete_minimal yields the shifted weak-Popov minimality, returning for any nonzero solution a dominating basis row. Supporting lemmas cover auxiliary properties such as zero-row characterizations (pm_rowGet_eq_zero_of_rowIsZero, pm_rowIsZero_of_rowGet, pm_rowIsZero_of_mem_rowSpan_all_zero), span transfer across zero-row compaction (pm_mem_rowSpan_of_nonzero_rows_mem, pm_mem_matrixRows_compactNonzeroRows, pm_mem_rowSpan_compactNonzeroRows), expansion of combination products (pm_combination_mul_toPoly), residual problem approximation (pm_rowApproximates_residual_of_combination), composition of row-linear combinations (pm_rowLinearCombination_combination), and the shifted weak-Popov shape of the final basis via pivot-row properties (pm_pivotRows_shiftedWeakPopov, pm_missingCompletionRows_facts, pm_completeMissingPivotRows_shiftedWeakPopov). No sorry or admit appear in the diff.
• CompPoly/LinearAlgebra/PolynomialMatrix/Approximant/PMBasis/KernelLeaf.lean: This new file adds the classical scalar-kernel PM-basis leaf for X-adic approximant problems. It defines the dense coefficient matrix (coefficientMatrix, coefficientMatrixRows) and its row‑array RREF (scalarRrefRows, scalarRrefRowsLoop), the homogeneous kernel basis from that RREF (homogeneousKernelBasisRows), and conversion of kernel vectors to polynomial rows (vectorToPolynomialRow). It also provides monomial completion rows (kernelLeafCompletionRows, missingCompletionRows, completeMissingPivotRows), shifted‑leading‑term conflict detection (kernelLeafConflict?, kernelLeafConflictInRow?, etc.), and two reduction strategies (reduceKernelLeafWithFuel with fuel‑bounded pair scans, and reduceKernelLeafRowsByPivots using a pivot‑table insertion). The incremental reduction variant (reduceKernelLeafRowsIncremental, insertKernelLeafRowIncremental) is used to keep the live basis small. The top‑level function kernelLeafBasis composes these steps: compute the scalar kernel, convert to polynomial rows, add completion rows, incrementally reduce, and fill missing pivot positions. No sorry or admit appear in the file.
• CompPoly/LinearAlgebra/PolynomialMatrix/Approximant/PMBasis/KernelLeafCompleteness.lean: Added new file KernelLeafCompleteness.lean containing the completeness proof for the kernel‑leaf basis generation. The file introduces auxiliary lemmas (pm_append_getD_left, pm_append_getD_right, pm_map_getD, pm_coeff_C_mul, pm_coeff_finset_sum, pm_coeff_mul_coeffXPower, pm_truncateX_eq_zero_of_coeff, pm_high_factor, pm_rowGet_monomialUnitRow, pm_completionRows_size, pm_completionRows_getD, pm_rowGet_rowLinearCombination, pm_rowLinearCombination_size, pm_row_ext, pm_rowApproximates_of_entry_dvd, pm_kernelLeafUnion_sizes, pm_reduceIncremental_sizes) and three main theorems (pm_lowRow_mem_rowSpan_union, pm_highRow_mem_rowSpan_union, pm_solution_mem_rowSpan_union) that decompose a solution row into low and high parts, each shown to be in the row span of the union of reconstructed scalar‑kernel rows and monomial completion rows. The culminating theorem kernelLeafBasis_rowSpan_complete proves that every nonzero solution row of an X‑adic problem lies in the row span of the kernel‑leaf basis. No sorry or admit appear.
• CompPoly/LinearAlgebra/PolynomialMatrix/Approximant/PMBasis/KernelLeafScalar.lean: This new file introduces the scalar kernel leaf for the PM‑basis, proving both soundness and completeness of the row‑array scalar RREF kernel used by the leaf. It defines scalarDot and OrthRows to express orthogonality, a ScalarRrefSpec structure that encodes the reduced row‑echelon shape invariants, and an elimStep for row operations. The main theorems homogeneousKernelBasisRows_size, homogeneousKernelBasisRows_dot_eq_zero, and homogeneousKernelBasisRows_complete establish that every emitted vector has the correct length, is orthogonal to all input rows, and that any vector orthogonal to those rows is an F‑linear combination of the emitted basis vectors. No sorry or admit appear in the file.
• CompPoly/LinearAlgebra/PolynomialMatrix/Approximant/PMBasis/KernelLeafSoundness.lean: This new file (KernelLeafSoundness.lean) proves the soundness of the kernel‑leaf basis for X‑adic approximants. The central theorem kernelLeafBasis_rows asserts that every row of kernelLeafBasis both satisfies RowApproximates and has size equal to problem.matrix.size. Supporting results establish invariant propagation through pivot insertion and reduction (insertKernelLeafPivotRowWithFuel_invariant, reduceKernelLeafRowsByPivots_invariant, reduceKernelLeafRowsIncremental_invariant), the identity between a polynomial row and its packed coefficient vector (vectorToPolynomialRow_rowToCoefficientVector), and the converse coefficient‑bridge (coefficientMatrixRows_dot_eq_zero_of_approximates) that turns an approximating row into orthogonality with all scalar coefficient rows. Several private lemmas (pm_foldl_push_toList, pm_doubleFoldl_toList, pm_sum_range_mul, coefficientMatrixRow_getD, mem_coefficientEquationIndices and its bounds variant) support the main arguments. No sorry or admit appear; all proofs are complete.
• CompPoly/LinearAlgebra/PolynomialMatrix/Approximant/PMBasis/KernelLeafSpan.lean: Summary unavailable — AI generation failed.
• CompPoly/LinearAlgebra/PolynomialMatrix/Approximant/PMBasis/Recursion.lean: This new file introduces the recursive PM-basis driver for the fast computation of matrix-type Padé approximants. It defines the core data structure PMBasisRuntime (holding multiplication contexts, composition/residual-product functions, leaf cutoff, and the leaf solver), three concrete runtime constructors kernelLeafRuntimeWithLowAndCompose, kernelLeafRuntimeWithLow, and kernelLeafRuntime (which plug in the scalar dense-kernel routine and Strassen-based low-level multiplication), the fuel-bounded recursive driver pmBasisWithFuelCore (which decomposes the problem by halving the maximal order, recurses on the lower and residual subproblems, applies compaction after each leaf and composition step, and documents why internal nodes avoid re-reduction for cost-model reasons), the root normalization pmBasisNormalizeRoot (one weak-Popov reduction pass via reduceKernelLeafRows and completeMissingPivotRows), and the public entry points pmBasisWithFuel (fuel-bounded with normalization), pmBasisFuel (default fuel equal to maxOrder + 1), and pmBasis (the top-level entry point). The file also provides two size-positivity theorems (completeMissingPivotRows_size_pos and pmBasisNormalizeRoot_size_pos) and the packaging structure PMBasisContext that bundles the runtime, the pmBasis operation, and the sound and complete_minimal proof obligations (stated but given only as ∀ propositions, not yet proved). No sorry or admit appear in the diff.
• CompPoly/LinearAlgebra/PolynomialMatrix/Approximant/PMBasis/XAdicSoundness.lean: This new file defines the RowApproximates predicate for X-adic approximant conditions and proves its closure under the row operations used in kernel leaf reduction and completion steps. Key theorems include rowApproximates_iff (divisibility characterization), rowApproximates_rowSub, rowApproximates_rowScaleCoeffX, and rowApproximates_cancelKernelLeafLeadingTerm for closure under subtraction, coefficient-shift scaling, and leading-term cancellation. It also proves insertKernelLeafPivotRowWithFuel_approximates, reduceKernelLeafRowsByPivots_approximates, and completeMissingPivotRows_approximates for pivot table operations, and rowApproximates_monomialUnitRow for monomial unit rows. The central result is rowApproximates_composed, which establishes soundness of one PM-basis composition step: a residual-approximant row multiplied by a lower-approximant basis approximates the full problem. No sorry or admit appear in the proofs.
• CompPoly/LinearAlgebra/PolynomialMatrix/Approximant/PartialLinearization.lean: This is a new file, PartialLinearization.lean (235 lines), which introduces executable helpers for sizing the expanded X-adic problem in diagonal modular-equation solvers using partial linearization. It defines the structures PrincipalChunk and PartialLinearizationPlan, along with numerous supporting functions: ceilDivFallback, modulusDegreeMass, chunkDelta, linearizedOrders, maxShiftDegree, principalShiftOffset, quotientShift, liftedPrincipalShift, exactNullspaceShift, principalChunkCount, principalChunks, principalUnitChunks, fallbackPivotDegree, pivotDegreeAt, principalChunkCountFromPivotDegree, principalChunksFromPivotDegrees, and three plan builders (partialLinearizationPlan, partialLinearizationPlanFromPivotDegrees, unchunkedPartialLinearizationPlan). It also provides polynomial-shifting primitives (xPowPolynomial, shiftPolynomialX, shiftRowX) and compression functions for chunked rows and bases (chunkedExactNullspaceShift, compressChunkedPrincipalRow, compressChunkedPrincipalRows). No sorry or admit appear in the diff.
• CompPoly/LinearAlgebra/PolynomialMatrix/MuldersStorjohannCorrectness/Fast.lean: The diff makes two small adjustments in CompPoly/LinearAlgebra/PolynomialMatrix/MuldersStorjohannCorrectness/Fast.lean. In the module-level docstring, the phrasing "once per scan" is refined to "once per conflict scan" to more precisely describe when the fast reducer caches shifted leading positions. In the inductive case of muldersStorjohannReduceWithFuelFast_eq, the anonymous binder | some _ is replaced with a named binder | some pair; this is a cosmetic change that makes the matched value syntactically available (though pair is not used in the simp only block on the right‑hand side), likely as a preparation for a future proof step or to improve readability. No theorems, definitions, or logical content are added or removed.
• CompPoly/LinearAlgebra/PolynomialMatrix/MuldersStorjohannCorrectness/Reduction.lean: Added theorem muldersStorjohannReduceWithFuel_eq_of_no_conflict that shows determinism of the fueled reducer: if two runs with possibly different fuel both produce a matrix with no shifted leading conflict (i.e., shiftedLeadingConflict? returns none), then the resulting matrices are equal. This formalizes that the reduction stabilizes once a conflict-free matrix is reached, independent of remaining fuel.
• CompPoly/LinearAlgebra/PolynomialMatrix/MuldersStorjohannCorrectness/WeakPopovMinimal.lean: This new file WeakPopovMinimal.lean adds two theorems establishing the predictable-degree property for shifted weak-Popov matrices. shiftedWeakPopov_least_row_minimal proves that for any well-formed shifted weak-Popov matrix B and any row in its row span (with defined shifted degree), there is a row of B whose shifted degree is a lower bound. muldersStorjohannReduce_least_row_minimal_of_weakPopov then deduces the same property for the output of muldersStorjohannReduce using existing lemmas about the reducer preserving well-formedness, weak-Popov property, and row span. The file contains no sorry or admit.
• CompPoly/LinearAlgebra/PolynomialMatrix/Operations.lean: This new file adds a comprehensive library of executable polynomial matrix operations for the CompPoly formalization. It defines truncateX for X‑adic truncation (with the truncateX_coeff theorem describing its coefficient behavior), the MulLowContext structure for low‑product multiplication, and multiple matrix multiplication entry points (mulWith, mul, mulStrassenWith, mulTruncColumnStrassenWith) that support explicit multiplication contexts, Strassen’s algorithm, and per‑column truncation. It also includes modular reduction (modByMonicWith, rowModDiagonalWith, modDiagonalWith), rectangular block extraction (block, joinSquareBlocks, padSquare, trimShape), helper functions for computing degree caps and exponents, and a row‑selection routine (leastShiftedDegreeRow?) for shifted‑degree scanning. No sorry or admit appear in the file.
• CompPoly/LinearAlgebra/PolynomialMatrix/RowSelection.lean: This new file CompPoly/LinearAlgebra/PolynomialMatrix/RowSelection.lean is added. It defines the predicate RowChoiceValid and proves a series of private theorems about the internal leastShiftedDegreeRowStep? and leastShiftedDegreeFold helpers, including that they preserve degree bounds and produce none only when there is no candidate row. It then uses these to prove the public theorems leastShiftedDegreeChoice?_some_valid, leastShiftedDegreeChoice?_degree_le, leastShiftedDegreeChoice?_some_of_degree, and leastShiftedDegreeRow?_some_valid, which establish correctness properties of the leastShiftedDegreeChoice? and leastShiftedDegreeRow? functions from the Operations module. No sorry or admit are present.
• CompPoly/LinearAlgebra/PolynomialMatrix/StrassenCorrectness.lean: This new file adds correctness proofs for the Strassen-style polynomial-matrix multiplication algorithms defined in CompPoly.LinearAlgebra.PolynomialMatrix.Operations. It introduces the main theorems mulStrassenWith_eq_mulWith and mulTruncColumnStrassenWith_eq_truncateColumns, which respectively establish that the Strassen recursion (with fuel) and its column-truncated variant compute exactly the same result as the naive matrix product (as arrays). Supporting lemmas formalize properties of truncateX, ofFn matrix construction, array helpers, and the Strassen seven-product sum identities (strassen_sum₁₁, strassen_sum₁₂, strassen_sum₂₁, strassen_sum₂₂), as well as padding and trimming steps (pad_step, trunc_pad_step). No sorry or admit appear in the diff.
• ROADMAP.md: The ROADMAP.md bullet for the Guruswami-Sudan list-decoding implementation was updated to add approximant-basis (PM-Basis) and hybrid interpolation as additional backend-parametric interpolation methods, alongside the previously listed dense and Lee-O'Sullivan options, reflecting the expanded set of implemented algorithms in the project.
• docs/wiki/coding-theory.md: Added documentation for two new interpolation backends — ApproximantBasis (quasi-linear in code length, corruption-independent) and Hybrid (budgeted Lee–O’Sullivan with fallback to approximant) — both of which produce a ValidInterpolationWitness. Noted a new WitnessDivisibility*.lean supporting quasi-linear multiplicity checks via Hasse derivatives, and that named KoalaBear contexts for all four backends now live in Implementations.lean. Also added a new bibliography reference for the PM-Basis approximant methods used by PolynomialMatrix/Approximant/ and Interpolation/ApproximantBasis/. Updated descriptive text from 'both' to 'all' to reflect the expanded set of backends.
• tests/CompPolyTests.lean: Two new public import statements were added to the test suite index. The first exposes CompPolyTests.Bivariate.GuruswamiSudan.Interpolation.ApproximantBasis, which provides test coverage for the approximant basis construction used in the Guruswami–Sudan interpolation step. The second exposes CompPolyTests.LinearAlgebra.PolynomialMatrix.Approximant, which tests the polynomial matrix approximant functionality. Both additions ensure these modules are included in the public test interface for the project.
• tests/CompPolyTests/Bivariate/GuruswamiSudan/Interpolation/ApproximantBasis.lean: This new test file provides executable coverage for the approximant-basis Guruswami–Sudan interpolation module. It defines private abbreviations and parameters (F3, F5, several GSInterpParams instances, point sets including duplicate x‑coordinates and non‑codeword variants) and constructs the corresponding GSModularData, PMBasisContext, ModularSolutionBasisContext, and GSInterpContext values. A series of #guard assertions then verify: interpolation parameter computations (interpolationYCap, interpolationWidth, interpolationShifts), distinct‑x‑coordinate detection, structural invariants of modular data (modulus counts, matrix dimensions, row entries), and that approximantBasisInterpolate returns a valid interpolationWitnessIsValidBool for multiple parameter/point scenarios (including duplicate x‑coordinates, low‑degree parameters, and non‑codeword stress configurations). Finally, it checks that gsCore returns at most three roots. No sorry or admit appear in the file.
• tests/CompPolyTests/LinearAlgebra/PolynomialMatrix/Approximant.lean: This new file adds a battery of #guard-based tests for the X-adic approximant problem pipeline in PolynomialMatrix.Approximant. It exercises problem and equation construction (problem, fullRankProblem, equation), matrix operations (kernelLeafBasis, mulStrassenWith, pmBasis), partial-linearization plan generation (partialLinearizationPlan, profileChunkPlan, noChunkPlan), chunked row compression (compressChunkedPrincipalRow), exact nullspace lifts (exactNullspaceLift, chunkedExactNullspaceLift), and end-to-end solution basis functions (knownDegreeSolutionBasisViaPMBasis, filteredSolutionBasisViaPMBasis, debugUnchunkedFilteredSolutionBasisViaPMBasis), together with auxiliary definitions (F3 field, X polynomial, moduli, pivot degree profiles) that serve as inputs to these checks.